Nuprl Lemma : rel_plus_functionality_wrt_iff
11,40
postcript
pdf
T
:Type,
R
,
Q
:(
T
T
).
(
x
,
y
:
T
. (
R
(
x
,
y
))
(
Q
(
x
,
y
)))
(
x
,
y
:
T
. (
R
^+(
x
,
y
))
(
Q
^+(
x
,
y
)))
latex
Definitions
R
^+
,
,
Type
,
P
Q
,
P
&
Q
,
P
Q
,
P
Q
,
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
x
f
y
,
f
(
a
)
,
rel_exp(
T
;
R
;
n
)
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
t
T
Lemmas
rel
exp
functionality
wrt
iff
,
nat
plus
inc
,
rel
exp
wf
origin
T:Type, R, Q:(T
T
).
x, y:T. (R(x,y)) 
(Q(x,y))) (x, y:T. (R^+(x,y)) (Q^+(x,y))) T:Type, R, Q:(TT).
x, y:T. (R(x,y)) (Q(x,y))) (x, y:T. (R^+(x,y)) (Q^+(x,y))) Q Q Q
B(x)
x:A. B(x)x:A. B(x)B(x)
T